RCS "$Id: ModalityComplex.sig,v 1.7 1998/08/13 11:38:51 pxs Exp $";
(* Complex modalities, which you can make from variables as well as    *)
(* lists of actions. *) 
signature MODALITY_COMPLEX =
  sig
    (* exn raised by satisfies when you ask a q whose answer depends *)
    (* on the value of some set. *)
    exception Dunno			
(* NB here, satisfies, filter raise Dunno if we can't tell. mentions says   *)
(* false in such a case (i.e. gives benefit of doubt!) *)

    type modality
    structure A : ACT
    val make : A.act list -> modality
    val negate : modality -> modality
    (* return true iff the action satisfies the modality, in the *)
    (* obvious sense.*) 
    val satisfies : A.act * modality -> bool
(* take a modality and a list of (act, 'a) pairs sorted by action, and *)
(* take advantage of the sorting to filter the list efficiently, returning *)
(* 'a list of things associated with actions which satisfy the modality. *)
    val filter : modality * (A.act * 'a) list ->
      'a list
    (* does the list inside the modality, pos or neg, refer to the action? *) 
    val mentions : modality * A.act -> bool
(* the boolean is true iff you want {} round lists of length >1. You   *)
(* never get them round lists of 0 or 1 actions. Tediously, it really  *)
(* does seem to be the convention to miss out {} inside [] or <>. *)
    val printString : bool -> modality -> string

    val makeFromVar : V.var -> modality
(* WARNING: this eq is not what you think! *)
(* simplistic equality test: they're equal iff syntactically       *)
    val eq: modality * modality -> bool
  end
